/**
 * @author	Jiefei Ma
 * @date		March 2010
 * Department of Computing, Imperial College London
 *
 * NOTE: this version can be run on SICStus4 or YAP6
 */




:- if(current_prolog_flag(dialect, yap)). 
%{
:- module(inequalities, [op(700, xfx, =/=), '=/='/2, inequalities/2]).
:- use_module(library(lists), [member/2, append/3]).
%} 
:- elif(current_prolog_flag(dialect, sicstus)). 
%{
:- module(inequalities, ['=/='/2, inequalities/2]).
:- op(700, xfx, =/=).
%}
:- endif.

:- use_module(library(atts)).
:- use_module(library(ordsets), [
		ord_union/3,
		list_to_ord_set/2
	]).

:- attribute aliens/1.

% public
X =/= Y :-
	(var(X) ; var(Y)), !,
	X \== Y, 
	reinforce_neq(X, Y),
	reinforce_neq(Y, X).
X =/= Y :-
	(unifiable(X, Y, Eqs) ->
		(Eqs = [A = B] ->
			A =/= B % no choice point
		;
			member(A = B, Eqs), % backtrackable
			A =/= B
		)
	;
		true
	).

unifiable(X, Y, [X = Y]) :-
	(var(X) ; var(Y)), !.
unifiable(X, Y, []) :-
	atomic(X), atomic(Y), !, X == Y.
unifiable(X, Y, Eqs) :-
	functor(X, F, A),
	functor(Y, F, A), 
	X =.. [F|ArgsX],
	Y =.. [F|ArgsY],
	all_unifiable(ArgsX, ArgsY, Eqs).
all_unifiable([], [], []).
all_unifiable([X|TX], [Y|TY], AllEqs) :-
	unifiable(X, Y, Eqs),
	all_unifiable(TX, TY, RestEqs),
	append(Eqs, RestEqs, AllEqs).

reinforce_neq(A, B) :-
	var(A), !,
	(get_atts(A, aliens(S)) ->
		(\+ strictmember(S, B) -> NewS = [B|S] ; NewS = S),
		put_atts(A, aliens(NewS))
	;
		put_atts(A, aliens([B]))
	).
reinforce_neq(_, _).

strictmember([H|T], X) :-
	(X == H ->
		true
	;
		strictmember(T, X)
	).

% hook
verify_attributes(Var, Val, Goals) :-
	get_atts(Var, aliens(S1)), !, % are we involved?
	\+ strictmember(S1, Val), % is it an alien?
	((var(Val), get_atts(Val, aliens(S2))) -> 
	% thanks Domenico Corapi for helping with fixing the bug, 2010/03/31
	%(var(Val) ->
		%get_atts(Val, aliens(S2)), 
		% \+ strictmember(S2, Var) % this should be implied by the previous test
		list_to_ord_set(S2, NewS2),
		list_to_ord_set(S1, NewS1),
		ord_union(NewS2, NewS1, S3), % copy forward aliens
		put_atts(Val, aliens(S3)),
		Goals = []
	;
		generate_goals(S1, Val, Goals)
	).
verify_attributes(_, _, []).

generate_goals([], _, []).
generate_goals([H|T], Val, Gs) :-
	generate_goals(T, Val, Gs1),
	(var(H) ->
		Gs = Gs1
	;
		Gs = [(Val =/= H)|Gs1]
	).

% hook
attribute_goal(Var, Goal) :-
	get_atts(Var, aliens(S)),
	list_to_ord_set(S, S1),
	construct_body(S1, Var, Goal).

construct_body([H|T], Var, Goal) :-
	(T = [] ->
		Goal = (Var =/= H)
	;
		construct_body(T, Var, G),
		Goal = ((Var =/= H),G)
	).

% public
inequalities(Var, Ineqs) :-
	get_atts(Var, aliens(S)), !,
	list_to_ord_set(S, S1),
	collect_inequalities(S1, Var, Ineqs).
inequalities(_, []).

collect_inequalities([], _, []).
collect_inequalities([H|T], Var, [N|Rest]) :-
	(Var @=< H ->
		N = (Var =/= H)
	;
		N = (H =/= Var)
	),
	collect_inequalities(T, Var, Rest).
